Inference at * 2 0 1 1 1 
Iof proof for Lemma multiply nat wf:



1. i : 
2. j : 
3. j < 0
4. ((j+1)  0 )  (0  (i * (j+1)))
5. j  0 
  0  (i * j) 

latex

 by Arith 

latex

 1: .....wf..... NILNIL

 1:   (i * j)  
 2: .....wf..... NILNIL

 2:   0  
 .

Definitions

s = t, n+m, #$n, , , x:AB(x), Void, a < b, n * m, t  T, False, P  Q, A, A  B, i  j